Step of Proof: lt_int_eq_false_elim_sqequal 12,41

Inference at * 1 2 
Iof proof for Lemma lt int eq false elim sqequal:

.....wf..... NILNIL

1. i : 
2. j : 
  (i <z j ~ ff)  Type 
latex

 by MemCD 
latex


 1: .....subterm..... T:t1:n

 1:   i <z j ~ i <z j
 2: .....subterm..... T:t2:n

 2:   ff ~ ff
 .


Definitionst  T
Lemmasint sq

origin